;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Itrim
  (sig trim (x))
  (sig trim-list-of-strs (strs))
  
  (con stringp-of-trim
       (implies (stringp (trim x)))
       :hints(("Goal" :in-theory (enable trim)))
       :rule-classes ((:rewrite)
                      (:type-prescription)))
  
)